active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
F(active(X1), X2) → F(X1, X2)
ACTIVE(h(X)) → G(X, X)
H(active(X)) → H(X)
G(mark(X1), X2) → G(X1, X2)
MARK(g(X1, X2)) → G(mark(X1), X2)
MARK(b) → ACTIVE(b)
ACTIVE(f(X, X)) → H(a)
ACTIVE(g(a, X)) → F(b, X)
ACTIVE(h(X)) → MARK(g(X, X))
MARK(f(X1, X2)) → F(mark(X1), X2)
ACTIVE(a) → MARK(b)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
MARK(h(X)) → ACTIVE(h(mark(X)))
F(X1, mark(X2)) → F(X1, X2)
ACTIVE(f(X, X)) → MARK(h(a))
MARK(g(X1, X2)) → MARK(X1)
G(active(X1), X2) → G(X1, X2)
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
MARK(a) → ACTIVE(a)
MARK(f(X1, X2)) → MARK(X1)
G(X1, mark(X2)) → G(X1, X2)
G(X1, active(X2)) → G(X1, X2)
MARK(h(X)) → MARK(X)
ACTIVE(g(a, X)) → MARK(f(b, X))
H(mark(X)) → H(X)
MARK(h(X)) → H(mark(X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(active(X1), X2) → F(X1, X2)
ACTIVE(h(X)) → G(X, X)
H(active(X)) → H(X)
G(mark(X1), X2) → G(X1, X2)
MARK(g(X1, X2)) → G(mark(X1), X2)
MARK(b) → ACTIVE(b)
ACTIVE(f(X, X)) → H(a)
ACTIVE(g(a, X)) → F(b, X)
ACTIVE(h(X)) → MARK(g(X, X))
MARK(f(X1, X2)) → F(mark(X1), X2)
ACTIVE(a) → MARK(b)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
MARK(h(X)) → ACTIVE(h(mark(X)))
F(X1, mark(X2)) → F(X1, X2)
ACTIVE(f(X, X)) → MARK(h(a))
MARK(g(X1, X2)) → MARK(X1)
G(active(X1), X2) → G(X1, X2)
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
MARK(a) → ACTIVE(a)
MARK(f(X1, X2)) → MARK(X1)
G(X1, mark(X2)) → G(X1, X2)
G(X1, active(X2)) → G(X1, X2)
MARK(h(X)) → MARK(X)
ACTIVE(g(a, X)) → MARK(f(b, X))
H(mark(X)) → H(X)
MARK(h(X)) → H(mark(X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F(active(X1), X2) → F(X1, X2)
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(active(X1), X2) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
Used ordering: Polynomial interpretation [25,35]:
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
The value of delta used in the strict ordering is 1.
POL(active(x1)) = 4 + (4)x_1
POL(mark(x1)) = 2 + (4)x_1
POL(F(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
The value of delta used in the strict ordering is 4.
POL(active(x1)) = 4 + (4)x_1
POL(mark(x1)) = 1 + x_1
POL(F(x1, x2)) = (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(X1, active(X2)) → G(X1, X2)
G(X1, mark(X2)) → G(X1, X2)
G(mark(X1), X2) → G(X1, X2)
G(active(X1), X2) → G(X1, X2)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(X1, active(X2)) → G(X1, X2)
G(X1, mark(X2)) → G(X1, X2)
Used ordering: Polynomial interpretation [25,35]:
G(mark(X1), X2) → G(X1, X2)
G(active(X1), X2) → G(X1, X2)
The value of delta used in the strict ordering is 1.
POL(active(x1)) = 1/4 + (4)x_1
POL(mark(x1)) = 4 + (2)x_1
POL(G(x1, x2)) = (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(mark(X1), X2) → G(X1, X2)
G(active(X1), X2) → G(X1, X2)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(mark(X1), X2) → G(X1, X2)
G(active(X1), X2) → G(X1, X2)
The value of delta used in the strict ordering is 4.
POL(active(x1)) = 4 + (4)x_1
POL(mark(x1)) = 1 + x_1
POL(G(x1, x2)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
H(active(X)) → H(X)
H(mark(X)) → H(X)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(active(X)) → H(X)
H(mark(X)) → H(X)
The value of delta used in the strict ordering is 4.
POL(active(x1)) = 1 + x_1
POL(H(x1)) = (4)x_1
POL(mark(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(h(X)) → ACTIVE(h(mark(X)))
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
MARK(f(X1, X2)) → MARK(X1)
MARK(h(X)) → MARK(X)
ACTIVE(f(X, X)) → MARK(h(a))
ACTIVE(h(X)) → MARK(g(X, X))
ACTIVE(g(a, X)) → MARK(f(b, X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
MARK(g(X1, X2)) → MARK(X1)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X1, X2)) → MARK(X1)
Used ordering: Polynomial interpretation [25,35]:
MARK(h(X)) → ACTIVE(h(mark(X)))
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
MARK(h(X)) → MARK(X)
ACTIVE(f(X, X)) → MARK(h(a))
ACTIVE(h(X)) → MARK(g(X, X))
ACTIVE(g(a, X)) → MARK(f(b, X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
MARK(g(X1, X2)) → MARK(X1)
The value of delta used in the strict ordering is 1/8.
POL(active(x1)) = x_1
POL(MARK(x1)) = (1/2)x_1
POL(a) = 1/4
POL(g(x1, x2)) = x_1
POL(f(x1, x2)) = 1/4 + x_1
POL(h(x1)) = x_1
POL(mark(x1)) = x_1
POL(b) = 0
POL(ACTIVE(x1)) = (1/2)x_1
mark(a) → active(a)
active(a) → mark(b)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(h(X)) → active(h(mark(X)))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(h(X)) → mark(g(X, X))
mark(g(X1, X2)) → active(g(mark(X1), X2))
h(active(X)) → h(X)
h(mark(X)) → h(X)
mark(b) → active(b)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
g(mark(X1), X2) → g(X1, X2)
f(X1, active(X2)) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MARK(h(X)) → ACTIVE(h(mark(X)))
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
MARK(h(X)) → MARK(X)
ACTIVE(f(X, X)) → MARK(h(a))
ACTIVE(h(X)) → MARK(g(X, X))
ACTIVE(g(a, X)) → MARK(f(b, X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
MARK(g(X1, X2)) → MARK(X1)
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(h(X)) → MARK(X)
MARK(g(X1, X2)) → MARK(X1)
Used ordering: Polynomial interpretation [25,35]:
MARK(h(X)) → ACTIVE(h(mark(X)))
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(h(a))
ACTIVE(h(X)) → MARK(g(X, X))
ACTIVE(g(a, X)) → MARK(f(b, X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
The value of delta used in the strict ordering is 1.
POL(active(x1)) = x_1
POL(MARK(x1)) = (1/4)x_1
POL(a) = 0
POL(g(x1, x2)) = 4 + (4)x_1
POL(f(x1, x2)) = 4
POL(h(x1)) = 4 + (4)x_1
POL(mark(x1)) = x_1
POL(b) = 0
POL(ACTIVE(x1)) = (1/4)x_1
mark(a) → active(a)
active(a) → mark(b)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(h(X)) → active(h(mark(X)))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(h(X)) → mark(g(X, X))
mark(g(X1, X2)) → active(g(mark(X1), X2))
h(active(X)) → h(X)
h(mark(X)) → h(X)
mark(b) → active(b)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
g(mark(X1), X2) → g(X1, X2)
f(X1, active(X2)) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
MARK(h(X)) → ACTIVE(h(mark(X)))
MARK(g(X1, X2)) → ACTIVE(g(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(h(a))
ACTIVE(h(X)) → MARK(g(X, X))
ACTIVE(g(a, X)) → MARK(f(b, X))
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
active(h(X)) → mark(g(X, X))
active(g(a, X)) → mark(f(b, X))
active(f(X, X)) → mark(h(a))
active(a) → mark(b)
mark(h(X)) → active(h(mark(X)))
mark(g(X1, X2)) → active(g(mark(X1), X2))
mark(a) → active(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(b) → active(b)
h(mark(X)) → h(X)
h(active(X)) → h(X)
g(mark(X1), X2) → g(X1, X2)
g(X1, mark(X2)) → g(X1, X2)
g(active(X1), X2) → g(X1, X2)
g(X1, active(X2)) → g(X1, X2)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)